Here we show that reduction preserves the well typedness of processes, to this aim we need three auxiliary lemmata. The first one handles substitutions.

\begin{lemma}[Substitution]\label{lem:substitution}
\begin{enumerate}
 \item If $\env{\Gamma}{ \Theta} \vdash P:\type{\Phi}{\Delta}$ then $\env{\Gamma}{ \Theta} \vdash P\sub{c'}{c}:\type{\Phi\sub{c'}{c}}{\Delta}$. 
  \item If $\env{\Gamma}{ \Theta} \vdash P:\type{\Phi}{\Delta}$ then $\env{\Gamma}{ \Theta} \vdash P\sub{\tilde{e}}{\tilde{x}}:\type{\Phi}{\Delta}$. 

  \item If $\judgebis{\env{\Gamma}{ \Theta,X:\type{\Phi'}{\Delta'}}}{P}{\type{\Phi}{\Delta}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi'}{\Delta'}}$ then $\judgement{\Gamma}{\Theta}{P\sub{Q}{X}}{\Phi}{\Delta}$.
   \item If $\judgebis{\env{\Gamma}{ \Theta,\mathsf{X}:\Delta'}}{P}{\type{\Phi}{\Delta}}$ and $\judgebis{\env{\Gamma}{\Theta}}{Q}{\type{\Phi'}{\Delta'}}$ then $\judgement{\Gamma}{\Theta}{P\sub{Q}{\mathsf{X}}}{\Phi}{\Delta}$.
\end{enumerate}
\end{lemma}



The second lemma allows to reverse typing rules and it follows from the definition of the typing system.
\begin{lemma} \label{lem:types} \quad \\
\begin{enumerate}
 \item \label{types1} if $\judgement{\Gamma}{\Theta}{P \parallel Q}{\Phi}{\Delta}$ then there exists $\Phi_1, \Phi_2, \Delta_1, \Delta_2$  such that $\judgement{\Gamma}{\Theta}{P}{\Phi_1}{\Delta_1}$,  $\judgement{\Gamma}{\Theta}{Q}{\Phi_2}{\Delta_2}$, $\Phi= \Phi_1 \bowtie  \Phi_2$ and $\Delta = \Delta_1 \uplus \Delta_2$;
 \item \label{types2} if $\judgement{\Gamma}{\Theta}{\inC{c}{\tilde{x}}.P}{\Phi}{\Delta}$ then there exists $\rho$  such that $\Phi = \Phi', c:?(\tilde{\kappa}).\rho $ and  $\judgement{\Gamma, \tilde{x}:\tilde{\kappa}}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;
 \item \label{types3} if $\judgement{\Gamma}{\Theta}{\outC{c}{\tilde{e}}.P}{\Phi}{\Delta}$ then there exists $\rho$  such that $\Phi = \Phi', c:!(\tilde{\kappa}).\rho $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;

 \item \label{typesdelin} if $\judgement{\Gamma}{\Theta}{\catch{c}{d}.P}{\Phi}{\Delta}$ then there exist $\rho, \sigma$  such that $\Phi = \Phi', c:?(\sigma).\rho $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho, d:\sigma}{\Delta}$;
 \item \label{typesdelout} if $\judgement{\Gamma}{\Theta}{\throw{c}{d}.P}{\Phi}{\Delta}$ then there exists $\rho, \sigma$  such that $\Phi = \Phi', c:!(\sigma).\rho, d:\sigma $ and  $\judgement{\Gamma}{\Theta}{P}{\Phi', c:\rho}{\Delta}$;
 
 \item \label{types4} if $\judgement{\Gamma}{\Theta}{\rec{X:\type{\Phi}{\Delta}}{P}}{\Phi}{\Delta}$ then  $\judgement{\Gamma}{\Theta, X:\type{\Phi}{\Delta}}{P}{\Phi}{\Delta}$;
 \item \label{types5} if $\judgement{\Gamma}{\Theta}{\ifte{e}{P}{Q}}{\Phi}{\Delta}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$,  $\judgement{\Gamma}{\Theta}{Q}{\Phi}{\Delta}$ and $\Gamma \vdash e:\mathsf{bool} $;
  \item \label{types6} if $\judgebis{\env{\Gamma}{\Theta}}{\component{l}{n}{\Delta}{P} }{ \type{\Phi}{\Delta}}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$ and $n = \#\{c \mid c:\omega \in \Phi\}$;
   \item \label{types7} if $\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{U}}{\type{\emptyset}{ \emptyset}}$ then $\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:\type{\emptyset}{\Delta_1}}}{ U}{\type{\emptyset}{ \Delta_2 }}$;
   \item \label{types8} if $\judgebis{\env{\Gamma}{\Theta}}{\nopen{a}{c:\rho}.P}{ \type{\Phi}{\Delta,\rho}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho}{ \Delta}}$;
   \item \label{types9} if $\judgebis{\env{\Gamma}{\Theta}}{ \close{c}.P}{ \type{\Phi}{ \Delta}}$ then there exists $\Phi'$ with $c\notin \dom{\Phi'} $ such that $\Phi = \Phi', c:\epsilon$ and $\judgebis{\env{\Gamma}{\Theta}}{ P}{\type{\Phi}{\Delta}}$;
   \item \label{types10} if $\judgement{\Gamma}{\Theta}{\restr{c}{P}}{\Phi}{\Delta}$ and $c\notin \dom{\Phi}$ then $\judgement{\Gamma}{\Theta}{P}{\Phi}{\Delta}$;
   \item \label{types11} if $\judgebis{\env{\Gamma}{\Theta}} {\restr{c}{P}}{\type{\Phi, c:\bot}{ \Delta}}$ then $\judgebis{\env{\Gamma}{\Theta}}{P }{\type{\Phi, c:\bot }{ \Delta}}$;
   \item \label{types12} if $\judgebis{\env{\Gamma}{\Theta}}{\branch{c}{n:P \dots n:P}}{\type{ \Phi}{ \Delta}}$ then there exists  $\Phi'$ such that $\Phi= \Phi', c:\&\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k \}$ and $\judgebis{\env{\Gamma}{\Theta}}{P_i}{\type{\Phi', c:\rho_i}{ \Delta}}$;
   \item \label{types13} if $\judgebis{\env{\Gamma}{\Theta}}{\select{c}{n_i}.P}{\type{\Phi}{\Delta}}$ then there exists  $\Phi'$ such that $\Phi= \Phi', \oplus\{n_1:\rho_1 \vee \dots \vee n_k:\rho_k$ and $\judgebis{ \env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho_i}{ \Delta}}$.
\end{enumerate}
\end{lemma}

The third lemma allows the introduction of contexts.  It follows  by induction on the sstructure  of the context using  Lemma \ref{lem:types}.
\begin{lemma}\label{lem:context}
Given a process $P$ and a context $C$, if $\judgement{\Gamma}{\Theta}{C[P]}{\Phi}{\Delta}$ then there exists $\Gamma', \Theta', \Phi', \Delta'$ such that $\judgement{\Gamma'}{\Theta'}{P}{\Phi'}{\Delta'}$.
\end{lemma}

